n, b:.  {0..n}{0..b} ~ {0..exp(b;n)} 

latex

Definitions

, t  T, x:AB(x), {i..j},  A ~ B, x:A. B(x), {x:A| B(x)} , P  Q, i  j , False, A, A  B, #$n, -n, n+m, n - m, a < b, Void, , exp(i;n), b, s = t, , x:A  B(x), P & Q, P  Q, Unit, left + right, Bij(A;B;f), i  j < k, S  T, suptype(S; T), x:A. B(x), f(a), <a, b>, x.A(x), , Surj(A;B;f), Inj(A;B;f), x. t(x), t.1, t.2, True, T, P  Q, Dec(P), b, (i = j), if b then t else f fi , {T}, SQType(T), s ~ t, n * m, primrec(n;b;c), P  Q, Type,

Lemmas

equipollent-multiply, exp wf, nat plus inc, nat plus wf, equipollent transitivity, product functionality wrt equipollent right, equipollent-zero, primrec wf, ifthenelse wf, eq int wf, bnot wf, not wf, assert wf, decidable int equal, pi2 wf, pi1 wf, le wf, biject wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert of eq int, equipollent-void-domain, int seg wf, ge wf, nat properties, nat wf